home *** CD-ROM | disk | FTP | other *** search
/ Language/OS - Multiplatform Resource Library / LANGUAGE OS.iso / sml_nj / 93src.lha / src / basics / unify.sml < prev    next >
Encoding:
Text File  |  1993-01-27  |  6.3 KB  |  207 lines
  1. (* Copyright 1990 by AT&T Bell Laboratories *)
  2.  
  3. structure Unify: UNIFY =
  4. struct
  5.  
  6. (*** type unification ***)
  7.  
  8. open Types ErrorMsg TypesUtil List2
  9.  
  10. exception Unify of string
  11.  
  12.  
  13. (*************** misc functions *****************************************)
  14.  
  15. val eqLabel = Symbol.eq
  16.  
  17. fun ltLabel(l1,l2) = Symbol.name l1 < Symbol.name l2
  18.  
  19. fun is_ubound (UBOUND _) = true
  20.   | is_ubound _ = false;
  21.  
  22. (*
  23.  * tycon_eqprop tycon:
  24.  *
  25.  *    This function returns the eqprop of tycon for use in determining
  26.  * when a CONty is an equality type.
  27.  *
  28.  * Note: Calling this function on ERRORtyc produces an impossible
  29.  * because an ERRORtyc should never occur in a CONty and hence an eqprop
  30.  * of one of them should never be needed.
  31.  *
  32.  * Calling this function on a DEFtyc also produces an impossible because
  33.  * the current eqprop scheme is insufficiently expressive to describe
  34.  * the possibilities.  (Ex: first argument must be an eq type but not
  35.  * necessarily the second)  Because of this, it is currently necessary to
  36.  * expand DEFtyc's before checking for equality types.
  37.  *)
  38. fun tycon_eqprop (GENtyc{eq,...}) = !eq
  39.   | tycon_eqprop (RECORDtyc _)  = YES
  40.   | tycon_eqprop _ = impossible "tycon_eqprop"
  41.  
  42. (*
  43.  * fieldwise just1 just2 combine fields1 fields2:
  44.  *
  45.  *    This function merges two sorted lists of (label, type) pairs
  46.  * (sorted by label) into a single sorted list of (label, type) pairs.
  47.  * If (l1,t1) occurs in fields1 but l1 doesn't occur in fields2 then
  48.  * (l1, just1 t1) occurs in the output.  Similarly with just2.
  49.  * If (l, t1) occurs in fields1 and (l,t2) in fields2, then 
  50.  * (l, combine t1 t2) occurs in the output.
  51.  *)
  52. fun fieldwise _ just2 _ [] fields2 = map (fn (n,t) => (n,just2 t)) fields2
  53.   | fieldwise just1 _ _ fields1 [] = map (fn (n,t) => (n,just1 t)) fields1
  54.   | fieldwise just1 just2 combine ((n1,t1)::r1) ((n2,t2)::r2) =
  55.     if eqLabel(n1,n2) then
  56.         (n1,combine(t1,t2))::(fieldwise just1 just2 combine r1 r2)
  57.     else if ltLabel(n1,n2) then
  58.         (n1,just1 t1)::(fieldwise just1 just2 combine r1 ((n2,t2)::r2))
  59.     else
  60.         (n2,just2 t2)::(fieldwise just1 just2 combine ((n1,t1)::r1) r2);
  61.  
  62.  
  63. (*************** adjust functions *****************************************)
  64.  
  65. fun adjust_variable eq depth weakness
  66.             (var2 as ref(OPEN{depth=d,eq=e,weakness=w,kind=k})) =
  67.     ((if is_ubound k then
  68.         (if weakness<w then
  69.         raise Unify "weakness violation"
  70.         else if eq andalso not e then
  71.         raise Unify "equality type required"
  72.         else
  73.         ()
  74.         )
  75.     else
  76.         ()
  77.     );
  78.         var2 := OPEN{depth=min(depth,d), eq=eq orelse e,
  79.              weakness=min(weakness,w), kind=k})
  80.    | adjust_variable _ _ _ _ = impossible "adjust_variable";
  81.  
  82. fun adjust_type (var as ref(OPEN{depth,eq,weakness,...})) ty =
  83.     let fun iter _ WILDCARDty = ()
  84.       | iter eq (VARty(ref(INSTANTIATED ty))) = iter eq ty
  85.       | iter eq (VARty(var' as ref(OPEN{kind=k,...}))) =
  86.         (if eqTyvar(var,var') then
  87.             raise Unify "circularity"
  88.         else
  89.             adjust_variable eq depth weakness var';
  90.             adjust_tvkind var k)
  91.       | iter eq (ty as CONty(DEFtyc _, args)) =
  92.         iter eq (headReduceType ty)
  93.        | iter eq (CONty(tycon,args)) =
  94.         (case tycon_eqprop tycon
  95.            of OBJ => app (iter false) args
  96.             | YES => app (iter eq) args
  97.             | _ => if eq then
  98.                  raise Unify "equality type required"
  99.              else
  100.                  app (iter false) args
  101.         )
  102.       | iter _ _ = impossible "adjust_type"
  103.     in iter eq ty end
  104.   | adjust_type _ _ = impossible "adjust_type"
  105.  
  106. and adjust_fields var fields = app (fn (l,t) => adjust_type var t) fields
  107.  
  108. and adjust_tvkind var (FLEX fields) = adjust_fields var fields
  109.   | adjust_tvkind var _ = ()
  110.  
  111.  
  112. (*************** unify functions *****************************************)
  113.  
  114. fun unifyTy(type1,type2) =
  115.     let val type1 = prune type1
  116.     val type2 = prune type2
  117.     in
  118.     (case (headReduceType type1, headReduceType type2) of
  119.           (WILDCARDty,_) => ()
  120.         | (_,WILDCARDty) => ()
  121.         | (VARty var1,VARty var2) =>
  122.         unify_variables var1 type1 var2 type2
  123.         | (VARty var1,etype2) =>
  124.         unify_variable var1 type2 etype2
  125.         | (etype1,VARty var2) =>
  126.         unify_variable var2 type1 etype1
  127.         | (CONty(tycon1,args1),CONty(tycon2,args2)) =>
  128.         if eqTycon(tycon1,tycon2) then
  129.             app2 unifyTy (args1,args2)
  130.         else
  131.             raise Unify "tycon mismatch"
  132.         | _ => raise Unify "type mismatch"
  133.         )
  134.     end
  135.  
  136. and unify_variables (var1 as ref(OPEN{depth=d1,eq=e1,weakness=w1,
  137.                       kind=k1}))
  138.             type1
  139.             (var2 as ref(OPEN{depth=d2,eq=e2,weakness=w2,
  140.                       kind=k2}))
  141.             type2 =
  142.     (if eqTyvar(var1,var2) then
  143.          ()
  144.      else (
  145.          adjust_type var1 (VARty var2);
  146.          adjust_type var2 (VARty var1);
  147.          let val new_info = OPEN{depth = min(d1,d2),
  148.                      eq = e1 orelse e2,
  149.                      weakness = min(w1,w2),
  150.                      kind = unify_tvinfos(k1,k2)};
  151.          in
  152.             (*
  153.              * This case is to prevent ever instantiating
  154.              * a UBOUND variable in unifying.  This is
  155.              * because certain other parts of the compiler
  156.              * depend on this not happening.
  157.              *)
  158.         case k1
  159.            of UBOUND _ => (var1 := new_info;
  160.                    var2 := INSTANTIATED type1)
  161.             | _        => (var1 := INSTANTIATED type2;
  162.                    var2 := new_info)
  163.          end
  164.      )
  165.     )
  166.    | unify_variables _ _ _ _ = impossible "unify_variables"
  167.  
  168. and unify_variable (var as ref(OPEN{kind=META,...})) ty _ =
  169.     (adjust_type var ty; var := INSTANTIATED ty)
  170.   | unify_variable (var as ref(OPEN{kind=FLEX fields,...})) ty
  171.            (CONty(RECORDtyc field_names, field_types)) =
  172.     let val record_fields = zip2 (field_names,field_types)
  173.     in
  174.         adjust_type var ty;
  175.         merge_fields false true fields record_fields;
  176.         var := INSTANTIATED ty
  177.     end
  178.   | unify_variable _ _ _ = raise Unify "type mismatch"
  179.  
  180. and unify_tvinfos(META,kind) = kind
  181.   | unify_tvinfos(kind,META) = kind
  182.   | unify_tvinfos(FLEX fields1, FLEX fields2) =
  183.     FLEX (merge_fields true true fields1 fields2)
  184.   | unify_tvinfos _ = raise Unify "bound type var"
  185.  
  186. (*
  187.  * merge_fields extra1 extra2 fields1 fields2:
  188.  *
  189.  *    This function merges the 2 sorted field lists.  Fields occuring
  190.  * in both lists have their types unified.  If a field occurs in only
  191.  * one list, say fields{i} then if extra{i} is true, an Unify error
  192.  * is raised.
  193.  *)
  194. and merge_fields extra1 extra2 fields1 fields2 =
  195.     let fun extra allowed = fn t => if not allowed then
  196.                          raise Unify "record labels"
  197.                     else
  198.                          t
  199.     in
  200.         fieldwise (extra extra1)
  201.               (extra extra2)
  202.               (fn (t1,t2) => (unifyTy(t1,t2); t1))
  203.               fields1 fields2
  204.     end
  205.  
  206. end (* structure Unify *)
  207.